\begin{tabbing}
(\=Auto THEN Subst' $n$ = 1+($n$ {-} 1) 0 THENA Auto') \+
\\[0ex]CollapseTHEN (
\-\\[0ex]RWO "primrec\_add" 0 THEN Auto THEN Reduce 0)$\cdot$
\end{tabbing}